Nuprl Lemma : mon_when_thru_op
13,42
postcript
pdf
g
:IMonoid,
b
:
,
p
,
q
:|
g
|. (when
b
. (
p
*
q
)) = ((when
b
.
p
) * (when
b
.
q
))
|
g
|
latex
Up
groups
1
Definitions of Statement
IMonoid
,
when
b
.
p
Definitions
ff
,
tt
,
t
T
,
if
b
then
t
else
f
fi
,
when
b
.
p
,
x
:
A
.
B
(
x
)
,
x
f
y
,
P
Q
,
P
&
Q
,
P
Q
,
P
Q
,
Unit
,
,
IMonoid
,
Lemmas
imon
wf
,
bool
wf
,
grp
car
wf
,
grp
op
wf
,
mon
ident
,
grp
id
wf
origin